COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%monadi[w85,jmc]		Decidability of monadic predicate calculus
C00012 ENDMK
C⊗;
%monadi[w85,jmc]		Decidability of monadic predicate calculus

\input jmcmac.tex[1,smc]
\title{A Normal Form for Monadic Formulas}

\vskip .5 in

Abstract: A normal form is given for formulas of the monadic first
order predicate calculus.  The form is related to one given in
Behmann's 1922 proof of decidability (unread) and discussed in
exercise 39.6 of Church's {\it Mathematical Logic}.  It
came up in extending decidability to circumscription for
monadic formulas.  However, the main purpose of this note is
to present the monadic case as a prototype of parametrizable or decidable
cases yet to be precisely defined that will be useful in AI.
\bigskip
\whentexed{monadi.tex[w85,jmc]}
\eject

	First consider closed monadic formulas involving the
predicate symbols $P↓1,\ldots,P↓n$.  Each such formula $E$ is equivalent
to a formula $normal(E)$ that is propositional in the $2↑n$ {\it base} formulas
$L↓{\epsilon↓1\ldots \epsilon↓n}$
 defined by
$∃x.(¬)↑{\epsilon↓1}P↓1(x)∧\ldots∧(¬)↑{\epsilon↓n}P↓n(x)$.  Here the powers
of $¬$ mean that $¬$ is omitted if the power is $0$ and included
if the power is $1$.  That's our theorem.

	Intuitively, each $L↓{\epsilon↓1\ldots \epsilon↓n}$ says whether a
certain kind of element exists in an interpretation.  There are
$2↑n$ kinds of elements and an interpretation is characterized
by which kinds of elements exist.  The same is true for predicate
calculus in general, but then there are an infinite number of
kinds of elements.  Of course $normal(E)$ is often very much longer
than $E$.  If $E$ is a theorem, then $normal(E)$ will be a propositional
tautology in its constituents.

	In order to prove the theorem we must first generalize it
to include open formulas.  Suppose $w↓1,\ldots,w↓m$ are the free
variables of $E$.  There is still a propositional normal form, but in addition
to the base formulas
$L↓{\epsilon↓1\ldots \epsilon↓n}$,
$normal(E)$
may contain any of the $2↑nm$ formulas
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
defined by
$(¬)↑{\epsilon↓1}P↓1(w↓k)∧\ldots∧(¬)↑{\epsilon↓n}P↓n(w↓k)$
as propositional constituents.  We'll call them base formulas also
and will distinguish between closed and open base formulas when
there is a need to do so.

	The proof is by induction on the structure of the formula,
so we must prove that the representation is possible for literals
and that property is preserved when formulas are combined by $∧$ and $∨$
and prefixed by $¬$ and existential quantifiers.
%  In order to avoid
%so many subscripts, we shall state and prove precise theorems for
%the case of two predicates, but the general case works exactly in
%the same way.  The greater concreteness of the two predicate case
%adds more understanding than is lost by the specialization.

\noindent{\bf Theorem 1:}
Every first order predicate calculus formula involving
predicate symbols $P↓1,\ldots,P↓n$ and individual variables $w↓1,\ldots,w↓m$
is representable as a disjunction of conjunctions.  Each conjunct
is either an
$L↓{\epsilon↓1\ldots \epsilon↓n}$,
of the form
$¬L↓{\epsilon↓1\ldots \epsilon↓n}$
or one of the
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$.  Only one $R$ involving a particular
$w↓k$ can occur in a conjunction.  (Since the distinct $R$s are
contradictory, having two of them would make the conjunction always false
and therefore omittable).

1. Every elementary formula $P↓i(w↓k)$ is expressible in the stated
form.  For example, if $n=2$, we have
%
$$P↓1(w) ≡ (P↓1(w)∧P↓2(w)) ∨ (P↓1(w)∧¬P↓2(w)) ≡ R↓{00}(w)∨R↓{01}(w)$$.

2. If $E$ and $F$ are expressible then so is $E∨F$.  The disjunction
is merely longer.  Of course and duplicate conjuncts should be omitted.

3. If $E$ and $F$ are expressible then so is $E∧F$.  This requires
applying the distributive law of conjunction over disjunction and
may greatly lengthen the formula.  However, if any conjunct contains
different
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
with the same $w↓k$, it can be omitted since they are contradictory.

4. If $E$ is expressible then so is $¬E$.  This involves using
de Morgan's law and distributing.  Again it can get long and
again conjunctions with contradictory conjuncts must be omitted.

5. If $E$ is expressible then so is $∃w↓k.E$.  The quantifier
distributes over the terms of the disjunction and so is applied
to each conjunct separately.  Within a conjunct at most one
$R↓{\epsilon↓1\ldots \epsilon↓n}(w↓k)$
can occur, and the quantifier converts it into
$L↓{\epsilon↓1\ldots \epsilon↓n}$ leaving the other conjuncts untouched.

This concludes the proof.  Note that universal quantifiers had
to be converted to existentials according to $∀x → ¬∃x¬$ which
will lengthen the formulas when the $¬$s are distributed.

\noindent{Remarks:}

1. The theorem gives a parametrization of monadic formulas in the sense
that every monadic formula is a propositional combination of the base
formulas.  If we want to search a space of monadic formulas we can
reduce the search to one over propositional combinations of base formulas.

2. We regard this theorem as a prototype of results we believe exist
concerning parametrizable classes of formulas of interest to AI.  The
intuition is that in many AI problems, there are only a finite numbers
of kinds of individuals that need be considered.

3. In this connection the pure theory of equality provides another
instructive example.  The closed formulas are propositional combinations
of formulas $at-least(n)$ asserting the existence of at least $n$ elements
in the domain.  These formulas are not independent, but we could try to
make them independent by expressing them in terms of the independent
formulas $exactly(n)$ asserting the existence of exactly $n$ elements.  
This doesn't quite succeed for lack of a formula asserting the existence
of an infinity of elements.  We speculate that it might be useful to
admit such a ``virtual'' formula to some formalizations.

\vfil\end